2016-08-09

Лямбда Синтаксиси

У цій публікації я хочу зібрати всі лямбда-синтаксиси. Почну з відомих синтаксисів лямбди:

λ x . B x — нетипізований класичний
λ x : A , B x — в наукових статтях
λ (x: A) → B x — Morte, Henk
λ (x: A) , B x — Lean, Anders
(x: A) B x — LISP синтаксис Диб'єра
[x: A] B(x) — AUTOMATH де Брейна
fun (x: A) => B x — мови програмування, французька школа
fun (X) -> B(X) — Erlang

Классика використовується учнями, які розв'язують домашні завдання, у вікіпедії та в HOL/Isabelle. Другий синтаксис використовується в статтях по лямбда-численню, наприклад, Streicher використовує його, третій також часто використовується в статтях, наприклад, Pfenning. Синтаксис LISP був винайдений Диб'єром у його роботі про індуктивні сімейства. Але все це вірації AUTOMATH, де є [], що є там квантором. Є ще логічний синтаксис правил висновку, запропонований Макбрайдом в Епіграмі, але це, на мій погляд, занадто. Синтаксис, який використовується в сучасних мовах програмування, також включений, сюди максимально, тому що на ньому незручно писати статті. Ми вибрали як синтаксис обчислення лямбда в Henk той, де є і дужки, і стрілки. Ми будуємо нормальні лямбда-форми вертикально, як це робив Диб’єр, щоб побачити шаблон і глибину термів.

Окремо хотілося б відзначити сімейство синтаксису Caramel, автором якого є Maia Victor, нажаль файли Карамелі похоронені під майстер гілкою, але я знайшов. Цей синтаксис також використовувався в оглядовій статті про лямбда-кодування CPS-кодування з континуатором.


 cons  = (x list cons nil -> (cons x (list cons nil)))
 nil   = (cons nil -> (id nil))
 foldr = (cons nil list -> (list cons nil))
 seq   = (foldr comp id)
 do    = (comp seq reverse)
 take  = (n -> (n (r l -> (cons (head l) (r (tail l)))) (const nil)))

Як виглядають індуктивні типи можна умовно розділити на британську школу LCF/ML/HOL/Hope/Miranda/Haskell/Agda/Idris та американську школу LISP/ACL2/NuPRL/Lean.


 data List (A : Set) : Set where
      []  : List A
      _∷_ : (x : A) (xs : List A) → List A

 data List (A: *): * :=
      (Nil: List A)
      (Cons: A → List A → List A)

 data List (A: U): U :=
      nil
    | cons (x: A) (xs: List A)

 data List : (A: Type) -> Type
    | nil  : Nat
    | cons : (x:A, xs: List(A)) -> Nat